Simulation offers to the user the possibility of exploring the possible
executions (\emph{traces} from now on) of a \nusmv model. 
In this way, the user can get familiar with a model and can acquire
confidence with its correctness before the actual verification of
properties.
This section describes the basic features of simulation in
\nusmv. Further details on the simulation commands
can be found in the \NuSMV User Manual.


\section{Trace Strategies}
\label{Trace Strategies}
\index{Trace Strategies}
\index{Tracing!Strategies}

In order to achieve maximum flexibility and degrees of freedom in a
simulation session, \nusmv permits three different trace
generation strategies: deterministic, random and interactive.
Each of them corresponds to a different way a state is picked from a set 
of possible choices.
In deterministic simulation mode the first state of a set (whatever it is) is
chosen, while in the random one the choice is performed nondeterministically.
In these two first modes traces are automatically generated by \nusmv:
the user obtains the whole of the trace in a time without control over the generation
itself (except for the simulation mode and the number of states entered via
command line).

In the third simulation mode, the user has a complete control over traces generation
by interactively building the trace. During an interactive simulation session,
the system stops at every step, showing a list of possible future states: the
user is requested to choose one of the items. This feature is particularly
useful when one wants to inspect some particular reactions of the model to
be checked.
When the number of possible future states exceeds an internal limit,
rather than ``confusing'' the user with a choice from a high number of
possible evolutions, the system
asks the user to ``guide'' the simulation via the insertion of some further
constraints over the possible future states.
The system will continue to ask for constraints insertion until the number of
future states will be under the predefined threshold. 
The constraints entered during this phase are accumulated (in a logical
product) in a single big constraint. This constraint is used only for
the current step of the simulation and is discarded before the next step.
The system checks the expressions entered by the user and 
does not accept them whenever an inconsistency arises.
Cases of inconsistency (i.e. empty set of states) may be caused by:
\begin{itemize}
\item the entered expressions (i.e. \code{a~\&~\~~a});
\item the result of the entered expressions conjoined with previous accumulated ones;
\item the result of accumulated constraints conjoined with the set of possible 
future states.
\end{itemize}


\section{Interactive Mode}
\label{Interactive Mode}
\index{Interactive Mode}
\index{Tracing!Interactive Mode}

A typical execution sequence of a simulation session could be as follows. Suppose
we use the model described below.\\
\begin{alltt}
MODULE main
VAR
  request : boolean;
  state : \{ready,busy\};
ASSIGN
  init(state) := ready;
  next(state) := case
                   state = ready & request : busy;
                   1                       : \{ready,busy\};
                 esac;
\end{alltt}

As a preliminary step, this model has to read into the \nusmv system.
This can be obtained by executing the following commands (we assume that the model is
saved in file \filename{short.smv}):
\footnote{We assume that every \nusmv command is followed by a
\ret keystroke. In the following examples,
\nusmv commands are written {\nusmvtext{like this}} to
distinguish them from system output messages.}
\begin{alltt}
\shellprompt \shelltext{\nusmvtxt -int short.smv}
\nusmvprompt \nusmvtext{go}
\nusmvprompt
\end{alltt}

\subsection{Choosing an Initial State}
\label{Choosing an Initial State}
\index{Choosing an Initial State}
\index{Tracing!Choosing an Initial State}
In order to start the simulation, an initial state has to be
chosen. This can be done in three ways:
\begin{itemize}
\item by default, the simulator uses the \emph{current state} as a 
starting point of every new simulation; this behavior if possible only
if a current state is defined (e.g., if we are exploring a trace);
\cindex{goto\_state}
\item if command \command{goto\_state} is used,
the user can select any state of an already existent
trace as the \emph{current state};
\cindex{pick\_state}
\item if \command{pick\_state} is used, then 
the user can choose the starting state of the simulation among the
initial states of the model; this command has to be used when a
\emph{current state} does not exist yet (that is when the model has
not yet been processed or when the system has been reset).
\end{itemize}

At this point of the example \emph{current state} does not exist, and there
is no trace currently stored in the system. Therefore,
an item from the set of initial states
has to be picked using command \command{pick\_state}.
A simulation session can be started now, using the \command{simulate}
command.
\cindex{print\_current\_state}
Consider for instance the following simulation session:
\begin{alltt}
\shellprompt \shelltext{\nusmvtxt -int short.smv}
\nusmvprompt \nusmvtext{go}
\nusmvprompt \nusmvtext{pick\_state -r}
\nusmvprompt \nusmvtext{print\_current\_state -v}
Current state is 1.1
request = 0
state = ready
\nusmvprompt \nusmvtext{simulate -r 3}
*********  Starting Simulation From State  1.1  *********
\nusmvprompt \nusmvtext{show\_traces -t}
There is 1 trace currently available.
\nusmvprompt \nusmvtext{show\_traces -v}
#################### Trace number: 1 ####################
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 1.1 <-
    request = 0
    state = ready
-> State: 1.2 <-
    request = 1
    state = busy
-> State: 1.3 <-
    request = 1
    state = ready
-> State: 1.4 <-
    request = 1
    state = busy
\end{alltt}

\cindex{pick\_state}
Command {\bf pick\_state -r} requires to pick the starting state of the
simulation \emph{randomly} from the set of initial states of the model.
\cindex{simulate}
Command {\bf simulate -r 3} asks to build a three-steps simulation by 
picking randomly the next states of the steps.
\cindex{show\_traces}
As shown by command {\bf show\_traces -v}, 
the resulting trace contains 4 states (the initial one, and the three ones
that have been added by the random simulation).
We remark that the generated traces are numbered: every trace is
identified by an integer number, while every state belonging to a trace
is identified by a \emph{dot notation}: for example state $1.3$ is the
third state of the first generated trace.

\subsection{Starting a New Simulation}
\label{Starting a New Simulation}
\index{Starting a New Simulation}
\index{Tracing!Starting a New Simulation}
Now the user can start a new simulation by choosing a new starting state.
In the next example, for instance, the user extends trace 1 by first
choosing state $1.4$ as the \emph{current state} and by then running a random simulation
of length $3$.
\begin{alltt}
\nusmvprompt \nusmvtext{goto\_state 1.4}
The starting state for new trace is:
-> State 2.4 <-
    request = 1
    state = busy
\nusmvprompt \nusmvtext{simulate -r 3}
********  Simulation Starting From State  2.4  ********
\nusmvprompt \nusmvtext{show\_traces 2}
################### Trace number: 2 ###################
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 2.1 <-
    request = 1
    state = ready
-> State: 2.2 <-
    state = busy
-> State: 2.3 <-
    request = 0
-> State: 2.4 <-
    request = 1
-> State: 2.5 <-
    request = 0
-> State: 2.6 <-
    state = ready
-> State: 2.7 <-
\nusmvprompt
\end{alltt}
As the reader can see from the previous example, the new trace is
stored as trace $2$.
The user is also able to interactively choose the states of the trace he wants to build:
an example of an interactive simulation is shown below:
\begin{alltt}
\nusmvprompt \nusmvtext{pick\_state -i}

***************  AVAILABLE STATES  *************

================= State =================
0) -------------------------
    request = 1
    state = ready

================= State =================
1) -------------------------
    request = 0
    state = ready


Choose a state from the above (0-1): {\bf 1} \ret

Chosen state is: 1
\nusmvprompt \nusmvtext{simulate -i 1}
********  Simulation Starting From State  3.1  ********

***************  AVAILABLE FUTURE STATES  *************

================= State =================
0) -------------------------
    request = 1
    state = ready

================= State =================
1) -------------------------
    request = 1
    state = busy

================= State =================
2) -------------------------
    request = 0
    state = ready

================= State =================
3) -------------------------
    request = 0
    state = busy


Choose a state from the above (0-3): {\bf 0} \ret

Chosen state is: 0
\nusmvprompt \nusmvtext{show\_traces 3}
################### Trace number: 3 ###################
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 3.1 <-
    request = 0
    state = ready
-> State: 3.2 <-
    request = 1
\end{alltt}

\subsection{Specifying Constraints}
\label{Specifying Constraints}
\index{Specifying Constraints}
\index{Tracing!Specifying Constraints}
\cindex{pick\_state}
\cindex{simulate}
The user can also specify some constraints to restrict the
set of states from which the simulator will pick out. Constraints can
be set for both the \command{pick\_state} command and the \command{simulate}
command using option \commandopt{c}.  
For example the following command picks an initial state by defining
a simple constraint:
\begin{alltt}
\nusmvprompt \nusmvtext{pick\_state -c "request = 1" -i}

***************  AVAILABLE STATES  ***************

================= State =================
0) -------------------------
    request = 1
    state = ready


There's only one future state. Press Return to Proceed. \ret
Chosen state is: 0
\nusmvprompt \nusmvtext{quit}
\shellprompt 
\end{alltt}

Note how the set of possible states to choose has being restricted (in this case
there is only one future state, so the system will automatically
pick it, waiting for the user to press the \ret key).
We remark that, in the case of command \command{simulate}, the constraints
defined using option \commandopt{c} are ``global'' for the actual trace to be
generated, in the sense that they are always included in every step of
the simulation. They are hence complementary to the constraints entered
with the \command{pick\_state} command, or during an interactive
simulation session when the number of future states to be displayed is
too high, since these are ``local'' only to a single simulation step and
are ``forgotten'' in the next one.
%@node  CTL model checking, LTL model checking, Simulation, Tutorial
%  node-name,  next,  previous,  up
